/**
 * 
 */
package controller.solver;

import java.io.BufferedWriter;
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
import java.util.List;
import java.util.StringTokenizer;

import model.solver.ImportESolver;
import model.solver.ImportSolverParameter;
import model.solver.SolverParameter;
import model.solver.SolverResult;
import model.solver.SolverResultStatus;
import controller.xml.XMLBaliseFormat;

/**
 * An {@link ImportSolver} is a solver that has been added to the application, but not in the
 * traditional way. There is not specific code for this solver, it use the generic implementation of
 * {@link Solver}. The solver must respect the requirement of the SAT SOLVER COMPETITION
 * http://www.satcompetition.org/2009/format-solvers2009.html .
 * 
 * @author GRONOWSKI Stephane svan001@aol.com
 * 
 *         igsat 2010
 * 
 */
public class ImportSolver extends SolverModel {

	public static final String		UNKNOWN_TOKEN		= "UNKNOWN";
	public static final String		SAT_TOKEN			= "SATISFIABLE";
	public static final String		UNSATISFIABLE_TOKEN	= "UNSATISFIABLE";

	public static final String		VALUE_TOKEN			= "v ";
	public static final String		COM_TOKEN			= "c ";
	public static final String		SOLUTION_TOKEN		= "s ";

	private ImportSolverParameter	param;
	private ImportSolverParameter	defaultParam;
	private ImportESolver			type;

	/**
	 * 
	 * Create a {@link ImportSolver}.
	 * 
	 * @param type
	 *            {@link ImportESolver} of the solver
	 * @param directory
	 *            directory where the executable file is.
	 * @throws IOException
	 *             if there is a problem with the file.
	 */
	public ImportSolver(ImportESolver type, File directory) throws IOException {
		super(type.getDescription(), type.getSatReturnValue(), type.getUnsatReturnValue());

		defaultParam = type.getDefaultParam();
		param = defaultParam.copy();
		this.type = type;

		if (!directory.isDirectory() || !new File(directory, type.getExecution()).isFile())
			throw new IllegalArgumentException();

		try
		{
			path = directory.getCanonicalPath() + File.separator + type.getExecution();
		} catch (IOException e)
		{
			e.printStackTrace();
			throw new IOException();
		}
	}

	/**
	 * Export the data in XML
	 * 
	 * @param file
	 *            {@link BufferedWriter} to write
	 * @throws IOException
	 */
	@Override
	public void exportXML(BufferedWriter file) throws IOException {

		// open
		// file.newLine();
		file.write("<" + XMLBaliseFormat.SOLVER + ">");

		// type
		// file.newLine();
		file.write("<" + XMLBaliseFormat.SOLVER_TYPE + ">");
		file.write(type.getXmlValue());
		file.write("</" + XMLBaliseFormat.SOLVER_TYPE + ">");

		// param
		getSolverParameter().exportXML(file);

		// close
		// file.newLine();
		file.write("</" + XMLBaliseFormat.SOLVER + ">");
	}

	/**
	 * Return the {@link ImportESolver}.
	 * 
	 * @return the type
	 */
	public ImportESolver getTypeImport() {
		return type;
	}

	/**
	 * Set the parameter.
	 * 
	 * @param param
	 *            the param to set
	 */
	public void setParam(ImportSolverParameter param) {
		this.param = param;
	}


	/**
	 * Return the default {@link ImportSolverParameter}.
	 * 
	 * @return the defaultParam
	 */
	public ImportSolverParameter getDefaultParam() {
		return defaultParam;
	}

	/**
	 * Set the default {@link ImportSolverParameter}.
	 * 
	 * @param defaultParam
	 *            the defaultParam to set
	 */
	public void setDefaultParam(ImportSolverParameter defaultParam) {
		this.defaultParam = defaultParam;
	}

	/**
	 * Return the current {@link ImportSolverParameter}.
	 * 
	 * @return the param
	 */
	public ImportSolverParameter getParam() {
		return param;
	}

	@Override
	public String[] getCommandLine(String cnfFile) {
		List<String> tmp = param.getParams();
		List<String> res = new ArrayList<String>();

		tmp.set(0, path);
		tmp.set(param.getCnfposition(), cnfFile);

		for (int i = 0 ; i < tmp.size() ; i++)
			if (!tmp.get(i).isEmpty())
				res.add(tmp.get(i));

		String[] command = new String[res.size()];
		for (int i = 0 ; i < res.size() ; i++)
		{
			System.out.println("arg: " + res.get(i));
			command[i] = res.get(i);
		}

		return command;
	}

	@Override
	public boolean hasTimeout() {
		return false;
	}

	@Override
	public boolean checkParameter() {
		return param.basicCheck();
	}

	@Override
	public SolverParameter getSolverParameter() {
		return param;
	}

	@Override
	public void setSolverParameter(SolverParameter param) {
		this.param = (ImportSolverParameter) param;
	}

	public void setImportParameter(ImportSolverParameter param) {
		this.param = param;
	}

	@Override
	protected void returnHasBeenStop(SolverResult res) {
		System.out.println("return stop");
	}

	@Override
	protected void returnHasBeenTimeout(SolverResult res) {
		System.out.println("return time");
	}

	@Override
	protected void returnProblem(SolverResult res) {
		System.out.println("return pb");

	}

	@Override
	protected void returnSat(SolverResult res) {
		System.out.println("return sat");
		checkResult(res);
	}

	@Override
	protected void returnUnSat(SolverResult res) {
		System.out.println("return unsat");
		checkResult(res);
	}

	@Override
	protected void returnUnknown(SolverResult res) {
		System.out.println("return unknown");
		checkResult(res);
	}

	/**
	 * Lunch the post execution treatment, get all the information formatted following the
	 * requirement of the SAT SOLVER COMPETITION
	 * (http://www.satcompetition.org/2009/format-solvers2009.html) using the stdout/stderr.
	 * 
	 * @param res
	 *            the {@link SolverResult} of the execution
	 */
	private void checkResult(SolverResult res) {
		// unknown par defaut
		res.setStatus(SolverResultStatus.UNKNOWN);

		// check les ligne de la sortie standart
		checkOuput(res.getStdout(), res);
		// check les ligne de la sortie des erreur
		checkOuput(res.getStderr(), res);
	}

	/**
	 * Check an output : search for the {@link SolverResultStatus}, the solution if sat, formatted
	 * following the requirement of the SAT SOLVER COMPETITION
	 * (http://www.satcompetition.org/2009/format-solvers2009.html) using the stdout/stderr.
	 * 
	 * @param output
	 *            the output to check
	 * @param res
	 *            the {@link SolverResult} to complete.
	 */
	private void checkOuput(String output, SolverResult res) {
		StringTokenizer tokenizer = new StringTokenizer(output, "\n", false);
		int max = tokenizer.countTokens();
		String token;
		String solution = res.getSolution();

		System.out.println("max = " + max);
		for (int i = 0 ; i < max ; i++)
		{// parcourir toute les lignes
			token = tokenizer.nextToken();
			if (token.startsWith(COM_TOKEN))
				continue;// commentaire

			if (token.startsWith(SOLUTION_TOKEN))
			{// solution
				System.out.println("solution trouver");
				if (res.getStatus() != SolverResultStatus.UNKNOWN)
				{// pb 2 status declarer
					System.out.println("pb");
					res.setStatus(SolverResultStatus.UNKNOWN);
					continue;
				}

				if (token.equals(SOLUTION_TOKEN + SAT_TOKEN))
				{// repond sat
					System.out.println("sat");
					res.setStatus(SolverResultStatus.SATISFIABLE);
					continue;
				}
				if (token.equals(SOLUTION_TOKEN + UNSATISFIABLE_TOKEN))
				{// repond unsat
					System.out.println("unsat");
					res.setStatus(SolverResultStatus.UNSATISFIABLE);
					continue;
				}
				// laisse par default unknown comme prevue par les regle de la competition
				System.out.println("solution non reconnu: " + token);
				continue;
			}

			if (token.startsWith(VALUE_TOKEN))
			{// affiche une solution
				System.out.println("value trouver");
				if (solution == null)
					solution = token.substring(VALUE_TOKEN.length());
				else
					solution.concat(token.substring(VALUE_TOKEN.length()));
				continue;
			}
			System.out.println("Ligne innatendu dans stdout: " + token);
		}

		if (solution != null)
			res.setSolution(solution);
	}

	@Override
	public String toString() {
		return description;
	}
}
